FDL - Nuprl Lemma : antecedent-function_functionality_wrt

Nuprl Lemma : antecedent-function_functionality_wrt_iff

es:ES, P, Q, P', Q':(E

), f:({e:E| P(e)}

{e:E| Q(e)} ).
(

e:E. (P(e))

(P'(e)))

(

e:E. (Q(e))

(Q'(e)))

P')

Definitions A c B, Q f P, t T, P Q, P & Q, P Q, P Q, , x:A. B(x)

Lemmas subtype rel function, event system wf, iff wf, es-E wf, antecedent-function wf

Definitions	A c B, Q f P, t T, P Q, P & Q, P Q, P Q, , x:A. B(x)
Lemmas	subtype rel function, event system wf, iff wf, es-E wf, antecedent-function wf